/******************************************************************************

    Copyright (C) 2006 Alessio Stalla (alessiostalla@gmail.com)

    This file is part of PrettyProlog.

    PrettyProlog is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    PrettyProlog is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with PrettyProlog; if not, write to the Free Software
    Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA

    See the file COPYING for further details.

 *****************************************************************************/

package prettyprolog.datatypes;

import java.io.Serializable;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Vector;

import prettyprolog.engine.Domain;
import prettyprolog.engine.Engine;

/**
 * A Substitution is a set of mappings between Variables and Terms.<br />
 * Substitutions can be composed forming new Substitutions; this is useful for
 * the unification mechanism, for example. The composition algorithm is
 * described in detail in the <code>compose()</code> method description.<br />
 * Throughout the documentation and the source code, mappings in Substitutions
 * are usually notated as <code>V = t</code>, meaning &quot;the variable
 * <code>V</code> gets replaces by <code>t</code>&quot;; that is, <code>=</code>
 * doesn't mean &quot;equals&quot;. Another less used notation with the same
 * meaning is <code>V &lt;-- t</code>.
 * @param <Vector>
 */
public class Substitution implements Serializable {

	private static final long serialVersionUID = 1L;
	
	protected HashMap<Variable, Term> map = new HashMap<Variable, Term>();
	
	/**
	 * Maps <code>v</code> with <code>t</code>.
	 * 
	 * @return <code>true</code> if the mapping is effectively estabilished,
	 *         <code>false</code> otherwise (i.e. the Substitution already
	 *         contained a mapping for <code>v</code>).<br />
	 *         The only exception is that if you try to map a Variable with
	 *         itself, no mapping is estabilished, but <code>true</code> is
	 *         returned.
	 */
	public boolean putMapping(Variable v, Term t) {
		if (map.get(v) != null && !map.get(v).equals(t))
//			System.out.println("C'e' gia!!! " + v + " " + t + " " + map.get(v));
		if (map.get(v) != null && !map.get(v).equals(t))
			return false;
		if (v.equals(t))
			return true;
		if (t instanceof Real) {
			int a = (int) ((Real) t).getValue();
			
			Vector temp1 = new Vector();	
			Vector temp2 = new Vector();	
			temp1.add(a);
//			v.dom = temp1;
//			Domain.updateDomain(v, temp1);
			Vector Adom = ((Variable) v).dom;
			if(!Adom.isEmpty()) {
				if(Adom.contains(a)) {
					v.dom = temp1;
					Domain.updateDomain(v, temp1);
//					System.out.println("Real " + v + " " + t + " " + v.dom);
				} else {
//					System.out.println("Real1 " + v + " " + t + " " + v.dom);
					v.dom = temp2;
					Domain.updateDomain(v, temp2);
				}
			} else {
				v.dom = temp1;
				Domain.updateDomain(v, temp1);
			}
/*			Vector dom = (Domain.getDomain((Variable) v));
			if (dom.contains(a)) {
				Vector temp = new Vector();
				temp.add(a);
				Domain.updateDomain((Variable) v, temp);
			} else {
				Vector temporal = new Vector();
				temporal.add(a);
				Domain.updateDomain((Variable) v, temporal);
			}		*/	
		}
		if (t instanceof Variable) {
			if (Domain.isDomain(v)) {
				Vector dom = v.getDomain();
				Vector dom1 = ((Variable) t).getDomain();
//				System.out.println("Var_v: "+v+" "+dom+"\n");
//				System.out.println("Var_v_dom: "+v+" "+v.dom+"\n");
//				System.out.println("Var_t: "+t+" "+dom1+"\n");
//				System.out.println("Var_t_dom: "+t+" "+((Variable) t).dom+"\n");
				Domain.updateDomain((Variable) t, dom);
//				System.out.println("Var_t: "+t+" "+((Variable) t).dom+"\n");
				((Variable) t).dom = dom;
				Vector dom2 = ((Variable) t).getDomain();
//				System.out.println("Var_t_n: "+t+" "+dom2+"\n");
//				System.out.println("Var_t_n_dom: "+t+" "+((Variable) t).dom+"\n");
			}
		}
//		if(!(t instanceof Real)) {
			map.put(v, t);
//		}
//		System.out.println("Variable: "+v.toString()+ " = "+t.toString()+"\n");
//		System.out.println("Var: "+v.toString()+ " = "+v.dom+"\n");
//		System.out.println("MAP1: "+map.toString()+"\n");
		v.setSubst(t);
		return true;
	}

	public Variable getVar (Term t) {
		Variable var = null;
//		System.out.println("MAP: "+map.toString()+"\n");
		for(Variable v : map.keySet()) {
			if(!v.toString().startsWith("_")) {
				Term temp = map.get(v);
				if (t.equals(temp)) {
					var = (Variable) v;
				}
			}
		}
		if(var == null) {
			Term temp = null;
			if (map.get(t) != null) {
				temp = map.get(t);
				var = getVar(temp);
			} else {
				var = ((Variable) t).getSubst();
			}
		}
		return var;
	}
	
	public Variable getSub (Term t) {
		Variable subst = (Variable) map.get(t);
		if (subst == null) {
			subst = (Variable) t;
		}
		return subst;
	}
	
	public Vector getVariabili() {
		Vector variabili = new Vector();
		for(Variable v : map.keySet()) {
			if(!v.toString().startsWith("_")) {
				variabili.add(v);
			}
		}
		return variabili;
	}
	
	public HashMap<Variable, Term> getMap() {
		return map;
	}
	
	
	
	public Vector getVarList() {			// da le variabili del goal con le correnti sostituzioni
		Vector temp = new Vector();
		for(Variable v : map.keySet()) {
			if(!v.toString().startsWith("_")) {
				if(!(map.get(v) instanceof Real)) {
					temp.add(0, map.get(v));
				}
			}
		}
		return temp;
	}

	
	public void refreshDom(Vector var) {
		for(int i=0; i < var.size(); i++) {
			Variable temp = (Variable) var.get(i);
			Term t = map.get(temp);
			Domain.updateDomain(temp, Domain.getDomain((Variable) t));
		}
	}
	
	public Term getSubst (Term var) {
		Term t = map.get(var);
		return t;
	}
	
	public Vector getVarValue(Vector var) {
		Vector temp = new Vector();
		for(int i=0; i < var.size(); i++) {
			temp.add(((Variable) var.get(i)).getValue());
		}
		return temp;
	}
	

	/** @return an Iterator over the Variables in this Substitution. */
	public Iterator<Variable> varIterator() {
		return map.keySet().iterator();
	}

	/** Equivalent to <code>putAll(subst, true)</code>. */
	public boolean putAll(Substitution subst) {
		return putAll(subst, true);
	}

	/**
	 * Attempts to add all of <code>subst</code>'s mappings into this
	 * Substitution. If <code>halt</code> is <code>true</code>, as soon as a
	 * mapping can't be put this method returns, else all mappings are inserted
	 * if possible.
	 * 
	 * @return <code>true</code> if all mappings were successfully put,
	 *         <code>false</code> otherwise.
	 */
	public boolean putAll(Substitution subst, boolean halt) {
		Iterator<Variable> it = subst.varIterator();
		boolean flag = true;
		while (it.hasNext()) {
			Variable var = it.next();
			if (!putMapping(var, subst.getValue(var))) {
				flag = false;
				System.out.println("Argh! mapping tra " + var + " e "
						+ subst.getValue(var));
				if (halt)
					return flag;
			}
		}
		return flag;
	}

	/**
	 * Composes this Substitution with the <code>other</code> one.<br />
	 * Composition works as follows:
	 * <ol>
	 * <li>First, an empty <code>Substitution s</code> is created.</li>
	 * <li>
	 * Then, for every mapping <code>v = t</code> in this Substitution, a
	 * mapping <code>v = t.apply(other)</code> is put into <code>s</code>.</li>
	 * <li>
	 * Finally, every mapping from <code>other</code> is inserted into
	 * <code>s</code> if possible.</li>
	 * </ol>
	 * 
	 * @return a newly allocated Substitution which is the composition of
	 *         <code>this</code> with <code>other</code>.
	 */
	public Substitution compose(Substitution other) {
		Substitution subst = new Substitution();
		Iterator<Variable> it = varIterator();
		while (it.hasNext()) {
			Variable v = it.next();
			Term t = map.get(v).apply(other);
			subst.putMapping(v, t);
		}
		subst.putAll(other, false);
		return subst;
	}

	/**
	 * @return <code>true</code> if this Substitution contains no mappings,
	 *         <code>false</code> otherwise.
	 */
	public boolean isEmpty() {
		return map.isEmpty();
	}

	/**
	 * @return the Term associated with <code>v</code>, or <code>null</code> if
	 *         it doesn't exist.
	 */
	public Term getValue(Variable v) {
		return map.get(v);
	}

	/**
	 * @return a printed representation for this Substitution. If
	 *         <code>show_temp</code> is <code>true</code>, temporary Variables
	 *         are printed, else they are omitted.
	 */
	
	
	public String toString(boolean show_temp) {
		boolean flag = false;
		StringBuffer str = new StringBuffer();
		for (Variable v : map.keySet()) {
			if (!v.isTemporary() || show_temp) {
				Term t = map.get(v);
				if (!(t instanceof Variable) || !((Variable) t).isTemporary() || show_temp) {
					if (flag)
						str.append(", ");
					flag = true;
					str.append(v + " = " + t);
				}
			}
		}
		if (flag)
			return str.toString();
		else
			return "true";
	}
	


	/** Same as <code>toString(true)</code>. */
	public String toString() {
		return toString(true);
	}

}